Talk:COS
Notes on a Calculus of Higher Order Broadcasts CHOCS p ::= x \;\; \Big| \;\; nil \;\; \Big| \;\; a?x.p \;\; \Big| \;\; a!p'.p \;\; \Big| \;\; \tau . p \;\; \Big| \;\; p + p' \;\; \Big| \;\; p \; | \; p' \;\; \Big| \;\; p \setminus x \;\; \Big| \;\; pS CHOBS q ::= x \;\; \Big| \;\; nil \;\; \Big| \;\; a??x.q \;\; \Big| \;\; a!!q'.q \;\; \Big| \;\; \tau . q \;\; \Big| \;\; q + q' \;\; \Big| \;\; q \; | \; q' \;\; \Big| \;\; q \setminus x \;\; \Big| \;\; qS CHOCS in CHOBS Attempt 1. Receive: \big[\!\big[ a?x.P \big]\!\big] \equiv a_T??.(a_R??.\big[\!\big[ a?x.P \big]\!\big] + a_R!!.a??x.\big[\!\big[ P \big]\!\big]) Send: \big[\!\big[ a!P_1.P_2 \big]\!\big] \equiv a_T!!.\big[\!\big[ a!P_1.P_2 \big]\!\big] + a_R??.a!!\big[\!\big[ P_1 \big]\!\big].\big[\!\big[ P_2 \big]\!\big] Attempt 2. Receive: A_R = a_T??.(l??.u??.A_R + l!!.a_R!!.a??x.u_T??.u!!.P(x)) Send: A_T = a_T!!.A_T + l??.(u??.A_T + a_R??.(l_T??.u_T??.u??.A_T + l_T!!.a!!P_1.u_T!!.u??.P_2)) Attempt 3. JasonCozens 22:50, March 17, 2010 (UTC) In CHOCS only 1 process can communicate at a time. This means all transmissions should lock out all other transmissions. a!P_1.P_2 \equiv l_T!!. . . Also if the process is not the transmitter it must be locked out: a!P_1.P_2 \equiv l_T??. . . + l_T!!. . . If the process is locked out it will return at some point to being itself: a!P_1.P_2 \equiv l_T??. . .u_T??.a!P_1.P_2 + l_T!!. . . The locking process must unlock all others: a!P_1.P_2 \equiv l_T??. . .u_T??.a!P_1.P_2 + l_T!!. . .u_T!!.P_2 Once the process has locked the transmission it can unlock the receiver channel: a!P_1.P_2 \equiv l_T??. . .u_T??.a!P_1.P_2 + l_T!!.a_R!!. . .u_T!!.P_2 If no receiver broadcasts, it reverts to the start: a!P_1.P_2 \equiv l_T??. . .u_T??.a!P_1.P_2 + l_T!!.a_R!!.(u_T!!.a!P_1.P_2 + a_R??. . .a!!P_2.a_U?? . .u_T!!.P_2) Now the receiver, is waiting for the receive to open: a?x.P \equiv a_R??.(a_L??. . .a_U??.a?x.P + a_L!!. . .a??x. . .a_U!!.u_T??.P) \begin{array}{rcl} \; | \; Q & \equiv & ( P \setminus K ) \; | \; ( Q \setminus K ) \\ \\ & & where \; K = \{ l_K, u_K, k \} \end{array} ---- 4a. For the active transmitter: # Get global lock. # Get local K lock. : a!P_1.P_2 \equiv l_T!!.l_K!!. . . For all passive transmitters: # Accept global lock # If local accept kill lock # Accept kill and die # If not killed accept kill unlock # Accept global unlock : a!P_1.P_2 \equiv l_T??.(u_T??.a!P_1.P_2 + l_K??.(u_K??.u_T??.a!P_1.P_2 + k??.nil)) Combining active and passive: : \begin{array}{rcl} a!P_1.P_2 & \equiv & l_T!!.l_K!!. \\ & & + l_T??.(u_T??.a!P_1.P_2 + l_K??.(u_K??.u_T??.a!P_1.P_2 + k??.nil)) \end{array} Now see if there are any receivers: : \begin{array}{rcl} a!P_1.P_2 & \equiv & l_T!!.l_K!!.a_{TR}!!.(a_{TR}!!.u_K!!.u_T!!.a!P_1.P_2 + a_{RT}??.a!!P_1.k!!.u_T!!.P_2 \\ & & + l_T??.(u_T??.a!P_1.P_2 + l_K??.(u_K??.u_T??.a!P_1.P_2 + k??.nil)) \end{array} # Ready to kill. : \begin{array}{rcl} a?x.P & \equiv & a_{TR}??.(a_{RT}??.a?x.P + a_{RT}!!.a??x.u_T!!.P) \\ & & + l_K??.(u_K.a?x.P + k??.nil) \end{array} Lambda calculus in CHOS \begin{array}{rcl} \big[\!\big[ x \big]\!\big] & \equiv & \lambda ! x . nil \\ \big[\!\big[ \lambda x . E \big] \! \big] & \equiv & \lambda ? x . \big[ \! \big[ E \big]\!\big] \\ \big[\!\big[ E \; F \big]\!\big] & \equiv & \big[\!\big[ E \big]\!\big] \; | \; \lambda ! . \big[\!\big[ F \big]\!\big] \end{array}